\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:Id, $T$:Type, $v$:$T$, ${\it ks}$:Knd List,\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]${\it ds}$ $\parallel$ $x$ : $T$
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ ${\it ks}$) $\Rightarrow$ isrcv($k$) $\Rightarrow$ $i$ $=$ destination(lnk($k$)))
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal(${\it da}$)
\\[0ex]$\Rightarrow$ \=R{-}state{-}var{-}init($i$;${\it ds}$;${\it da}$;$x$;$T$;$v$;${\it ks}$;${\it tr}$)\+
\\[0ex]$\Vdash$ ${\it es}$.\=es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)\+
\\[0ex]$\Rightarrow$ \=vartype($i$;$x$) $\subseteq\rho$ $T$\+
\\[0ex]\& \=$\forall$$e$@$i$.\+
\\[0ex]($x$ after $e$) $=$ es{-}trans{-}state{-}from\{i:l\}(${\it es}$;${\it ks}$;${\it tr}$;$v$;es{-}init(${\it es}$;$e$);$e$) $\in$ $T$
\\[0ex]\& (first($e$) $\Rightarrow$ ($x$ when $e$) $=$ $v$ $\in$ $T$)
\-\-\-\-
\end{tabbing}